Nuprl Lemma : list_n_wf
2,24
postcript
pdf
A
:Type,
n
:
.
A
List(
n
)
Type
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
A
List(
n
)
Lemmas
length
wf1
origin
A:Type, n:
. A List(n) 
Type A:Type, n:. A List(n) Type Tx:A. B(x)